COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 combi1.lsp[w84,jmc]	 Replacing lambda expressions by combinators
C00016 ENDMK
C⊗;
;;; combi1.lsp[w84,jmc]	 Replacing lambda expressions by combinators

;;; replaces a functional expression by a curried form with functions of
;;; one argument.  (curry '(λ (x y) (f x y))) → (λ x (λ y ((f x) y))).
;;; Note that the bound variables are no longer in lists.
;;; Both (λ (x) (f x)) and (λ x (f x)) are acceptable equivalent input.
(defun curry (e)
       (cond
	((atom e) e)
	((eq (car e) 'λ)
	 (cond
	  ;; allows for a single atom as bound variable of λ
	  ((atom (cadr e)) (list 'λ (cadr e) (curry (caddr e))))
	  ((null (cdr (cadr e))) (list 'λ (car (cadr e)) (curry (caddr e))))
	  (t (list 'λ 
		   (car (cadr e))
		   (curry (list 'λ (cdr (cadr e)) (caddr e)))))))
	((null (cdr e)) (error 'function_of_no_arguments))
	((null (cddr e)) (list (curry (car e)) (curry (cadr e))))
	(t (curry (cons (list (car e) (cadr e)) (cddr e))))))

;;; If e is an expression and  x  is a variable  mkcomb(e,x) is a combinatory
;(cnormalize (mkcomb '(λ x (λ y a)) 'z))

;;; expression which, applied to  x, is equivalent to the original expression.
;;; mkcomb requires its argument  e  in curried form.
(defun mkcomb (e x)
       (cond 
	((atom e) (if (eq e x) 'I (list 'K e)))
	((eq (car e) 'λ) (mkcomb (mkcomb (caddr e) (cadr e)) x))
	((absent x e) (list 'K e))
	((absent x (car e)) (list (list 'B (car e)) (mkcomb (cadr e) x)))
	((absent x (cadr e)) (list (list 'S (mkcomb (car e) x))
				   (list 'K (cadr e))))
	(t (list (list 'S (mkcomb (car e) x)) (mkcomb (cadr e) x)))))

;;; x is not a free variable of e
(defun absent (x e)
       (if (atom e)
	   (not (eq e x))
	   (if (eq (car e) 'λ)
	       (or (eq (cadr e) x)
		   (absent x (caddr e)))
	       (and (absent x (car e)) (absent x (cadr e))))))

;;; (scott e) is the result of replacing all λ-expressions in e by combinators.
(defun scott (e) (purge (curry e)))

(defun purge (e)
       (cond
	((atom e) e)
	((eq (car e) 'λ) (purge (mkcomb (caddr e) (cadr e))))
	(t (list (purge (car e)) (purge (cadr e))))))


;;; From combinators to λ-expressions

;;; converts a combinator expression to λ-calculus and normalizes
(defun normalize (e)
       (normalize1 (lambdaize e)))

;;; crudely replaces each combinator by its lambda-expression
(defun lambdaize (e)
       (sublis '((i . (λ x x))
		   (k . (λ x (λ y x)))
		   (b . (λ f (λ g (λ x (f (g x))))))
		   (s . (λ f (λ g (λ x ((f x) (g x))))))) e))

;;; normalizes a λ-expression in a top-down way.  Of course, it may diverge.
(defun normalize1 (e)
       (cond
	((atom e) e)
	((eq (car e) 'λ) (list 'λ (cadr e) (normalize1 (caddr e))))
	((atom (car e)) (list (car e) (normalize1 (cadr e))))
	((eq (caar e) 'λ) (normalize1 (sub1 (cadr e) (cadar e) (caddar e))))
	(t (let ((f (normalize1 (car e)))
		 (e1 (normalize1 (cadr e))))
		(if (eq (car f) 'λ)
		    (normalize1 (sub1 e1 (cadr f) (caddr f)))
		    (list f e1))))))

;;; Just subst but changes bound variables when needed
;;; to avoid capturing free variables in x.
(defun sub1 (x y z) (sub2 x y z (freevars x)))

;;; w is a list of forbidden variables that cannot be used as bound
(defun sub2 (x y z w)
       (cond 
	((atom z) (if (eq z y) x z))
	((not (eq (car z) 'λ)) (list (sub2 x y (car z) w)
				     (sub2 x y (cadr z) w)))
	((eq y (cadr z)) z)
	(t (if (not (memq (cadr z) w))
	       (list 'λ (cadr z) (sub2 x y (caddr z) w))
	       (let ((nv (newvar (cadr z) (append w (freevars (caddr z))))))
		    (list
		     'λ
		     nv
		     (sub2 x y (subst nv (cadr z) (caddr z)) w)))))))

;;; The free variables in the expression x.
(defun freevars (x) (freevars1 x nil nil))

;;; A satellite of freevars
(defun freevars1 (x bound free)
       (cond ((atom x) (if (or (memq x bound) (memq x free))
			   free
			   (cons x free)))
	     ((eq (car x) 'λ) (freevars1 (caddr x) (cons (cadr x) bound) free))
	     (t (freevars1 (cadr x) bound (freevars1 (car x) bound free)))))
       
;;; disassembles a variable with a symbolic and numeric part, e.g.
;;; (find-parts 'ab17) = (ab  17) and (find-parts 'ab) → (ab nil)
(defun find-parts (var)
       (do ((a (exploden var)
	       (cdr a))
	    (b () (cons (car a) b)))
	   ((or (null a)(and (< #o57 (car a))
			     (< (car a) #o100)))
	    (if (null a)
		(list (implode (reverse b)) nil)
		(list (implode (reverse b)) (readlist a))))))

;;; merge-parts is the inverse of find-parts
(defun merge-parts  (var num)
       (if (null num)
	   var
	   (implode (append (explode var)
			(exploden num)))))

;;; (newvar var list) is the simplest variable with the same symbolic part
;;; as  var, that doesn't co-incide with any variable on   list.
;;; a is simpler than a0 which is simpler than  a1, etc.
(defun newvar (var list)
       (let ((sym (car (find-parts var))))
	    (merge-parts sym (do ((l list (cdr l))
				  (m () (find-parts (car l)))
				  (u () (if (eq (car m) sym)
					    (cons (cadr m) u)
					    u)))
				 ((null l) (hole (if (eq (car m) sym)
						     (cons (cadr m) u)
						     u)))))))

;;; The satellite of newvar that actually finds the first hole.
(defun hole (u)
       (if (not (memq nil u))
	   nil
	   (do ((n 0 (1+ n)))
	       ((not (member n u)) n))))

;;; normalizes the top level of a combinator expression using the
;;; definitions of I, K, B, and S.
(defun topcnormalize (e)
       (cond
	((atom e) e)
	((eq (car e) 'i) (cadr e))
	((atom (car e)) e)
	((eq (caar e) 'k) (cadar e))
	((atom (caar e)) e)
	((eq (caaar e) 'b) (list (cadaar e) (list (cadar e) (cadr e))))
	((eq (caaar e) 's) (list (list (cadaar e) (cadr e))
				 (list (cadar e) (cadr e))))
	(t e)))

;;; normalizes a combinator expression top down.  Of course, it may run
;;; indefinitely if the expression has no normal form.
(defun cnormalize (e)
       (if (atom e)
	   e
	   (let ((e1 (topcnormalize e)))
		(if (not (eq e1 e))
		    (cnormalize e1)
		    (let ((ncare (cnormalize (car e)))
			  (ncadre (cnormalize (cadr e))))
			 (if (and (eq ncare (car e)) (eq ncadre (cadr e)))
			     e
			     (cnormalize (list ncare ncadre))))))))

;;; applies syntactic sugar to λ-expressions
;;; e.g. (landin '(λ x (λ y ((f x) y)))) ==> (λ (x y) (f x y))
(defun landin (e)
       (cond
	((atom e) e)
	((eq (car e) 'λ) (if 
			  (and (not (atom (caddr e)))
			       (eq (car (caddr e)) 'λ))
			  (landin
			   (list 'λ
				 (append (vars (cadr e))
					 (vars (cadr (caddr e))))
				 (caddr (caddr e))))
			  (list 'λ (vars (cadr e)) (landin (caddr e)))))
	((atom (car e)) (cons (car e) (mapcar #'landin (cdr e))))
	(t (append (landin (car e)) (mapcar #'landin (cdr e))))))

(defun vars (x) (if (atom x) (list x) x))

(setq Y '(λ f ((λ x (f (x x)))
	       (λ x (f (x x))))))

;;; successful tests
(cnormalize '((k a) x))
A 
(cnormalize '((k ((b f) g)) x))
((B F) G) 
(cnormalize '(((k ((b f) g)) x) y))
(F (G Y)) 

(sub1 '((g x) y) 'y '(λ x ((f y)(g x))))
(normalize1 '((λ x x) y))
(normalize1 '((λ x ((f x) y)) ((g x) y)))
(normalize1 '((λ x (λ y ((f x) y))) ((g x) y)))
(normalize '((k i) b))
(normalize '((s k) k))
;;; tests

(normalize (curry '(f x)))
(normalize (curry '(f x y)))
(normalize (curry '(λ (x y) (f x y))))
(absent 'x 'a)
(absent 'x '(f a))
(absent 'x '(f x))
(absent 'x '((λ x (f x)) (λ y (f y))))

(mkcomb 'a 'x)
(mkcomb 'x 'x)
(normalize '((B F) I))
(mkcomb '(f x) 'x)
(scott 'x)
(scott '(f x))
(scott '(f x y))
(curry '(λ (x y) (f x y)))
(cnormalize (scott '(λ (x y) (f x y))))
((S ((B B) ((B F) I))) (K I)) 
(scott '(λ (x y) (f x y)))
((S ((B B) ((B F) I))) (K I)) 
(scott '(λ (x y) (f x)))
((B K) ((B F) I)) 
(cnormalize '(((S ((B K) ((B F) I))) (K Y)) z))
(F Z) 
(cnormalize (scott '(λ (x y) (f x))))
((B K) ((B F) I)) 
(setq foo (curry '(λ (x y) (f x y a))))
(λ X (λ Y (((F X) Y) A))) 
(normalize (mkcomb foo 'x))
(λ Y (λ X (λ X0 (((F X) X0) A)))) 
(setq foo1 (curry '(λ (x y) (f x y))))
(λ X (λ Y ((F X) Y))) 
(mkcomb foo1 'x)
(K ((S ((B B) ((B F) I))) (K I))) 
(mkcomb '(λ y ((foo x) y)) 'x)
((S ((B B) ((B FOO) I))) (K I)) 
(cnormalize (mkcomb  '(λ x a) 'z))
(K (K A)) 
(sub2 'x 'y '(λ x (x0 y))'(x))
(λ X1 (X0 X)) 
(normalize (scott '(λ (x y) (f x y))))
(λ X (λ X0 ((F X) X0))) 
(normalize (scott '(λ (x y) (f x y a))))
(λ X (λ X0 (((F X) X0) A))) 

(normalize (list y '(λ z a)))
A 
(setq y1 '(λ F ((λ X (F (X X))) (λ X (F (X X))))))
(λ F ((λ X (F (X X))) (λ X (F (X X))))) 
(scott y1)
((S ((S ((B B) I)) (K ((S I) I)))) ((S ((B B) I)) (K ((S I) I)))) 
(curry y1)
(λ F ((λ X (F (X X))) (λ X (F (X X))))) 
(scott y)
((S ((S ((B B) I)) (K ((S I) I)))) ((S ((B B) I)) (K ((S I) I)))) 

(landin '(f x))
(F X) 
(landin '((f x) y))
(F X Y) 
(landin '(((f x) y) z))
(F X Y Z) 
(landin '(λ x (f x)))
(λ (X) (F X)) 
(λ (X Y) (F X Y)) 
(landin '(λ (x y) ((f x) y)))
(λ (X Y) (F X Y)) 
(landin '(λ x (λ y ((f x) y))))
(λ (X Y) (F X Y))